\section{Herbrandovské univerzum}

\begin{poznamka}
    V nasledujúcom texte budeme používať a medzi sebou zamieňať
    nasledujúce výrazy s rovnakým významom:
    ``nie je splniteľná'', 
    ``je sporná'' a
    ``je protirečivá''. Taktiež, občas budeme zamieňať medzi sebou
    aj ich negácie.
\end{poznamka}

\begin{definicia}[Herbrandovské univerzum množiny klauzúl]
    Nech $H_0$ je množina konštánt, ktoré sa vyskytujú v množine
    klauzúl $S$.
    Ak $S$ neobsahuje žiadnu konštantu, tak položíme $H_0=\{ a \}$,
    kde $a$ je nejaká konštanta.
    Ďalej definujme $H_{i+1}$ ako zjednotenie $H_{i}$ a množiny všetkých termov
    tvaru $f^{(n)}(t_1,\dots, t_n)$, kde $f^{(n)} \in S$ a
    $t_1, \dots, t_n \in H_i$.
    Množinu $H_i$ nazývame
    {\rm herbrandovské univerzum $i$-tej úrovne}.
    Herbrandovské univerzum množiny klauzúl definujeme ako zjednotenie
    cez všetky úrovne:
    \begin{equation*}
        H=\bigcup_{i=0}^{\infty} H_i
    \end{equation*}
\end{definicia}

\begin{priklad}
    Majme množinu klauzúl
    $S= \{ P(a),\ \neg P(x) \lor \neg P(f(x))\}$.
    Potom herbrandovské univerzá jednotlivých úrovní sú
    \begin{align*}
        H_0& = \{ a \} \\
        H_1& = \{ a,\ f(a) \} \\
        H_2& = \{ a,\ f(a),\ f(f(a)) \} \\
         \vdots\ \ &\\
        H_{\phantom{0}} &= \{ a,\ f(a),\ f(f(a),\ f(f(f(a))),\ \dots \}
    \end{align*}
\end{priklad}

\begin{priklad}
    Nech $S=\{P(x) \lor R(x),\ R(z),\ T(y) \lor \neg W(y) \}$, teda
    množina $S$ neobsahuje žiadnu konštantu.
    Preto kladieme $H_0 = \{ a \}$. Dostávame
    $H_0=H_1=\dots=H=\{a\}$.
\end{priklad}

\begin{priklad}
    Uvažujme množinu klauzúl $S=\{P(f(x),a,g(y), b)\}$. Potom
    %% FIXME: do nasledujuceho alignu som nevedel narvat split
    %% ak to niekto vie, nech to fixne
    \begin{align*}
        H_0 =& \{ a,\ b\} \\
        H_1 =& \{ a,\ b,\ f(a),\ g(a),\ f(b),\ g(b) \} \\
        H_2 =& \{ a,\ b,\ f(a),\ g(a),\ f(b),\ g(b),\
                f(f(a)),\ f(f(b)),\\
              &\quad f(g(b)),\ f(g(b)),\
                g(f(a)),\ g(f(b)),\ g(g(a)),\ g(g(b)) \}
    \end{align*}    
\end{priklad}

\begin{definicia}[Výraz]
    Pod pojmom výraz budeme chápať 
    term, množinu termov,
    klauzulu, množinu klauzúl,
    atóm, množinu atómov,
    literál, množinu literálov.
\end{definicia}

\begin{definicia}[Podvýraz]
    Podvýraz výrazu $F$ je ľubovoľný výraz, ktorý sa vyskytuje v $F$.
\end{definicia}

\begin{definicia}[Základný výraz]
    Ľubovoľný výraz, ktorý neobsahuje premenné, sa nazýva základný výraz
    (základný term, základný atóm, základná klauzula, základný literál, ...).
\end{definicia}

\begin{definicia}[Základná inštancia]
    Základnou inštanciou klauzuly $C$ z množiny klauzúl $S$ je klauzula,
    ktorú dostaneme zámenou všetkých premenných
    za prvky Herbrandovského univerza.
\end{definicia}

\begin{priklad}
    Majme množinu $S = \{P(x),\ Q(f(x)) \lor R(y) \}$ a majme klauzulu
    $C: P(x)$. 
    Herbrandovské univerzum $H$ je
    $H = \{ a,\ f(a),\ f(f(a)),\ f(f(f(a))),\ \dots \}$.
    Základné inštancie pre $C$ sú $P(a), P(f(a)), P(f(f(a))), \dots$.
\end{priklad}

\begin{definicia}[Herbrandovská báza]
    Nech $S$ je množina formúl. Potom množina atómov
    tvaru $P^{(n)}(t_1, \ldots, t_n)$ pre všetky $n$-árne predikáty,
    ktoré sa vyskytujú v $S$ a všetky termy $t_i$ z Herbrandovského univerza
    nazývame Herbrandovskou bázou $S$.
    Sú to atómy takého tvaru, že sa v nich nevyskytuje žiadna
    premenná.
\end{definicia}

Položme si otázku, čo znamená interpretovať množinu klauzúl $S$ na
Herbrandovskom univerze $H$. Musíme poznať hodnoty konštánt,
interpretáciu funkčných a predikátových symbolov. Budeme uvažovať
špeciálnu interpretáciu, takzvanú $H$-interpretáciu, pri ktorej
nebudeme interpretovať predikátové symboly (necháme si to ako keby na
neskôr).

\begin{definicia}[H-interpretácia]
    Nech $S$ je množina klauzúl. Ďalej nech $H$ je herbrandovské
    univerzum pre množinu klauzúl $S$ a $I$ je interpretácia v množine
    klauzúl $S$ nad $H$.
    Hovoríme, že interpretácia $I$ je herbrandovská interpretácia 
    (alebo tiež H-interpretácia), ak platí: 

    \begin{enumerate}
	\item Interpretácia $I$ zobrazuje všetky konštanty na samé
            seba, t.j. konštante $a \in S$ priradí tú istú konštantu $a \in H$.

	\item Nech $f^{(n)}$ je $n$-árny funkčný symbol a
            $h_1, \dots, h_n$ sú prvky herbrandovského univerza $H$.
            Potom funkciu $f$ budeme v $I$ realizovať ako funkciu,
            ktorá zobrazuje $(h_1, \dots, h_n) \in H^n$ na element
            $f^{(n)}(h_1,\dots,h_n) \in H$.
    \end{enumerate}
\end{definicia}

\begin{poznamka}
    Ako sme už spomínali, nekladieme žiadne obmedzenia 
    na interpretáciu predikátov.

    Uvažujme ako príklad množinu $A = \{ A_1, A_2, \dots \}$.
    Nech je to herbrandovská báza pre množinu klauzúl $S$.
    Herbrandovskú interpretáciu určíme tak, že $I$ zadáme ako
    $I=\{ m_1, m_2, \ldots \}$, kde
    $m_i$ bude buď $A_j$ (ak $A_j$ je pravdivé) alebo
    $\neg A_j$ (ak $A_j$ je nepravdivé).
\end{poznamka}

\begin{priklad}
    Majme množinu klauzúl $S=\{ P(x) \lor Q(x),\ R(f(y)) \}$.
    Herbrandovské univerzum je
    $H=\{a,\ f(a),\ f(f(a)),\ \ldots \}$.
    V $S$ sa vyskytujú unárne predikáty $P,Q,R$.
    Herbrandovská báza je potom
    \begin{equation*}
        A: \{ P(a),\ Q(a),\ R(a),\ 
            P(f(a)),\ Q(f(a)),\ R(f(a)),\ \dots\}.\footnote{
            Všimnime si, že v danej množine je aj $R(a)$, hoci
            by sme možno očakávali, že to musí začínať $R(f(a))$
            }
    \end{equation*}
    Môžeme mať nasledovné interpretácie:
    \begin{equation*}
        I_1: \{ P(a),\ Q(a),\ R(a),\ 
        P(f(a)),\ Q(f(a)),\ R(f(a)),\ \dots \}
    \end{equation*}
    teda, predikáty sú vždy pravdivé. Alebo
    \begin{equation*}
        I_2: \{ \neg P(a),\ \neg Q(a),\ \neg R(a),\ 
            \neg P(f(a)),\ \neg Q(f(a)),\ \neg R(f(a)),\ \dots \}
    \end{equation*}
    čiže predikáty nie sú nikdy pravdivé.
    Ďalšia možná interpretácia je
    \begin{equation*}
        I_3: \{ P(a),\ Q(a),\ \neg R(a),\ 
            P(f(a)),\ Q(f(a)),\ \neg R(f(a)),\ \dots \}
    \end{equation*}
    V zásade pre každú možnú kombináciu si vieme vytvoriť
    interpretáciu.
\end{priklad}


\medskip
Ďalšou úlohou bude k ľubovoľnej interpretácii nad ľubovoľným univerzom
priradiť Herbrandovskú interpretáciu a zaviesť príslušné tvrdenia a definície.

\begin{priklad}
    \label{prikl:interpretacia}
    Majme množinu klauzúl $S = \{ P(x),\ Q(y, f(y,a)) \}$.
    Nech je oblasť interpretácie $D = \{1,2\}$ a interpretujme
    konštanty, funkčné symboly a predikátové symboly podľa tabuľky
    \ref{tab:priklad-interpretacia}

    \begin{table}[h]
        %%% {{{
        \centering
        \begin{tabular}{|r||c|c|c|c|c|}
            \hline
            symbol & a & f(1,1) & f(1,2) & f(2,1) & f(2,2) \\
            \hline
            hodnota & 2 & 1 & 2 & 2 & 1 \\
            \hline
        \end{tabular}
        
        \medskip
        \begin{tabular}{|r||c|c|c|c|c|c|}
            \hline
            predikát & P(1) & P(2) & Q(1,1) & Q(1,2) & Q(2,1) & Q(2,2) \\
            \hline
            hodnota & true & false & false & true & false & true \\
            \hline
        \end{tabular}
        \caption{Interpretácia $I$ z príkladu
          \ref{prikl:interpretacia}}
        \label{tab:priklad-interpretacia}
        %%% }}}
    \end{table}

    Ideme určiť H-interpretáciu $I^*$, ktorá akýmsi spôsobom bude
    prislúchať našej interpretácii $I$. Najsôr si určíme bázu:
    \begin{equation*}
        A=\{ P(a),\ Q(a,a),\ P(f(a,a)),\ Q(a,f(a,a)),
            Q(f(a,a), a),\ \ldots \}
    \end{equation*}

    Hodnoty pre príslušné predikáty $I^*$ určíme pomocou zadaných tabuliek
    pre $I$:

    \begin{align*}
        P(a) &= P(2) = false \\
        Q(a,a) &= Q(2,2) = true\\
        P(f(a,a)) &= P(f(2,2)) = P(1) =true \\
        Q(f(a,a),a) &= Q(f(2,2),2) = Q(1,2) =true \\
        Q(a,f(a,a)) &= Q(1,f(2,2)) = Q(2,1) =false \\
        Q(f(a,a),f(a,a)) &= Q(f(2,2), f(2,2)) = Q(1,1) =false \\
    \end{align*}

    Interpretácia $I^*$ je teda
    \begin{equation*}
        I^* = \{ \neg P(a),\ Q(a,a),\ P(f(a,a)),\ 
            \neg Q(a,f(a,a)),\ Q(f(a,a),a),\ \ldots \}
    \end{equation*}
\end{priklad}

\begin{priklad}
    \label{prikl:interpretacia2}
    Môže nastať aj iný prípad -- majme množinu klauzúl $S$, ktorá neobsahuje
    konštantu: $S=\{P(x),\ Q(y,f(y,z)) \}$.
    Máme danú interpretáciu $I$ s oblasťou $D=\{1,2\}$ popísanú
    tabuľkou \ref{tab:prikl-interpretacia2}

    \begin{table}[h]
        %%% {{{
        \centering
        \begin{tabular}{|r||c|c|c|c|}
            \hline
            symbol & f(1,1) & f(1,2) & f(2,1) & f(2,2) \\
            \hline
            hodnota  & 1 & 2 & 2 & 1 \\
            \hline
        \end{tabular}
        
        \medskip
        \begin{tabular}{|r||c|c|c|c|c|c|}
            \hline
            predikát & P(1) & P(2) & Q(1,1) & Q(1,2) & Q(2,1) & Q(2,2) \\
            \hline
            hodnota & true & false & false & true & false & false \\
            \hline
        \end{tabular}
        \caption{Interpretácia $I$ z príkladu
          \ref{prikl:interpretacia2}}
        \label{tab:prikl-interpretacia2}
        %%% }}}
    \end{table}
   
    Tejto interpretácii budú zodpovedať dve H-interpretácie
    $I_1^*$ a $I_2^*$, pričom v prvej bude $a$ interpretované ako $1$ 
    a v druhej ako $2$.

    \newcommand{\phn}{\phantom{\neg}}
    \begin{align*}
        I_1^* &= \{ \phn P(a),\ \neg Q(a,a),\ P(f(a,a)),\ \neg Q(a,f(a,a)),\
            \neg Q(f(a,a),a),\ \dots \} \\
        I_2^* &= \{ \neg P(a),\ \neg Q(a,a),\ P(f(a,a)),\ \neg Q(a,f(a,a)),\
            \phn Q(f(a,a),a),\ \dots \}
    \end{align*}
    \def\phn{\undefined}
\end{priklad}

Teraz si formálne zavedieme, čo to znamená priradiť nejakej interpretácii $I$
zodpovedajúcu H-interpretáciu $I^*$:

\begin{definicia}[Zodpovedajúca H-interpretácia]
    Majme interpretáciu $I$ pre množinu klauzúl $S$ na oblasti
    interpretácií $D$. Interpretácii $I$ priradíme zodpovedajúcu
    H-interpretáciu $I^*$ nasledovne:
    Nech $h_1, h_2, \ldots, h_n$ sú prvky Herbrandovského univerza
    $H$.
    Nech každé $h_i$ sa zobrazí v interpretácii $I$ na prvok
    $d_i \in D$.
    Zoberme predikát $P^{(n)}$ z množiny klauzúl $S$.
    Definujeme splniteľnosť (a pravdivosť) predikátu $P$ v $I^*$
    nasledovne:
    $P^{(n)}(h_1,\dots,h_n)$ je pravdivý v $I^*$ práve vtedy keď je
    $P^{(n)}(d_1,\dots,d_n)$ pravdivý v $I$.
\end{definicia}

\begin{lema}
    \label{lema:h-interpretacia}
    Majme interpretáciu $I$ na oblasti $D$. Nech táto interpretácia
    vyhovuje množine klauzúl $S$. Potom ľubovoľná H-interpretácia $I^*$,
    ktorá je priradená (zodpovedá) $I$, taktiež vyhovuje množine klauzúl $S$.
\end{lema}

\begin{dokaz}
    Majme množinu klauzúl $S=\{C^{(1)}, C^{(2)}, \ldots , C^{(n)}\}$.
    Nech klauzula $C^{(i)}$ je nasledujúca disjunkcia literálov
    $C^{(i)} = L^{(i)}_1 \lor L^{(i)}_2 \lor \ldots \lor
        L^{(i)}_{r_i}$ pre $i=1,\ldots,n$.
    Ľubovoľný literál $L^{(i)}_j$ je buď atomická formula alebo
    jej negácia. Predpokladajme že interpretácia $I$ na univeze $D$
    vyhovuje množine klauzúl $S$. Potom musí byť pravdivý aspoň jeden
    literál v každej klauzule $C^{(i)}$.
    Lenže pre tieto literály
    $L^{(i)}_j$ platí
    $L^{(i)}_j = P^{(n)}(d_1,\dots,d_n)$ je pravdivé v $I$ a z toho
    dostávame $P^{(n)}(h_1, \dots, h_n)$ je pravdivé v $I^*$.
    Teda, ak $I$ vyhovuje množine klauzúl $S$, bude jej vyhovovať aj
    $I^*$.
    \\
\end{dokaz}

\begin{veta}
    Množina klauzúl $S$ nie je splniteľná práve vtedy,
    keď $S$ je nepravdivá pri všetkých H-interpretáciach $S$.
\end{veta}


\begin{dokaz}
    \noindent
    \begin{itemize}
    \item[$\Rightarrow:$] Nech množina klauzúl $S$ nie je splniteľná.
        Potom je nepravdivá pre ľubovoľnú interpretáciu na ľubovoľnej
        oblasti.
        Teda aj pre ľubovoľnú H-interpretáciu na H-univerze.

    \item[$\Leftarrow:$] Nech množina klauzúl $S$ je nepravdivá pre
        ľubovoľnú H-interpretáciu množiny klauzúl $S$.
        Pre spor predpokladajme, že existuje interpretácia $I$ 
        s oblasťou $D$ pre množinu klauzúl $S$, ktorá
        vyhovuje $S$.
        Uvažujme $I^*$, ktorá je priradená (zodpovedá) interpretácii
        $I$ pre množinu klauzúl $S$.
        Podľa lemy \ref{lema:h-interpretacia} ale vieme,
        že ak vyhovuje $I$, vyhovuje aj $I^*$, čo je spor.
    \end{itemize}
\end{dokaz}

Podarilo sa nám teda objaviť také univerzum (H-univerzum), pre ktoré
stačí vyšetriť splniteľnosť množiny klauzúl $S$ na všetkých
interpretáciach a budeme vedieť povedať (ne)splniteľnosť formuly na
ľubovoľnej interpretácii v ľubovoľnom univerze. Posunuli sme sa o krok
bližšie k rozhodovaniu platnosti $S$.

\begin{poznamka}
    V nasledujúcom texte budeme používať iba H-interpretácie.
    Preto sa dohodneme (na skrátenie a zjednodušenie zápisu), že
    ich budeme nazývať iba interpretácie a označovať ako $I$.
\end{poznamka}

\begin{poznamka}
    Zhrňme si niekoľko základných pozorovaní:
    \begin{enumerate}
	\item Majme klauzulu (disjunkciu literálov) $C$
            a nech $C'$ je jej základná inštancia, t.j. 
            každá premenná bola nahradená prvkom H-univerza.
            $C'$ je splniteľná v (H-)interpretácii $I$
	    práve vtedy, keď existuje základný literál $L' \in I$,
            ktorý je splniteľný.
            Teda $C'$ je splniteľná $\iff$ $C' \intersect I \ne 0$.            

	\item Klauzula $C$ je splnená v interpretácii $I$ $\iff$ každá jej
	    základná inštancia $C'$ je splnená v $I$.

	\item Klauzula $C$ je odmietnutá (vyvrátená) v $I$ $\iff$ existuje
	    aspoň jedna taká základná inštancia $C'$, ktorá 
            nie je splniteľná (teda je vyvrátená) v $I$.

	\item Množina klauzúl $S$ nie je splniteľná $\iff$ 
            pre každú interpretáciu $I$ existuje aspoň jedna klauzula
            $C\in S$ a jej základná inštancia $C'$, 
            ktorá nie je splniteľná v $I$.
    \end{enumerate}
\end{poznamka}

\begin{priklad}
    Uvažujme klauzulu $C=\neg P(x) \lor Q(f(x))$ a
    interpretácie $I_1,I_2,I_3$ definované nasledovne:
    \newcommand{\phn}{\phantom{\neg}}
    \begin{align*}
        I_1 &= \{ \neg P(a),\ \neg Q(a),\ \neg P(f(a)),\ 
            \neg Q(f(a)),\ \neg P(f(f(a))),\ \neg Q(f(f(a))),\ \dots \} \\
        I_2 &= \{ \phn P(a),\ \phn Q(a),\ \phn P(f(a)),\ 
            \phn Q(f(a)),\ \phn P(f(f(a))),\ \phn Q(f(f(a))),\ \dots \} \\
        I_3 &= \{ \phn P(a),\ \neg Q(a),\ \phn P(f(a)),\
            \neg Q(f(a)),\ \phn P(f(f(a))),\ \neg Q(f(f(a))),\ \dots \} \\
    \end{align*}
    \def\phn{\undefined}
    Všímajme si klauzulu $C$ a jednotlivé interpretácie:
    $I_1$ vyhovuje $C$ (inak povedané $C$ je splnená) a zabezpečujú to
    $\neg P(a),\ \neg P(f(a)),\ \neg P(f(f(a))), \dots$
    Podobne, $C$ je splnená v $I_2$ a zabezpečujú to
    $Q(a),\ Q(f(a)),\ Q(f(f(a))), \dots$ Naopak, $C$ nie je
    splniteľná v $I_3$.
\end{priklad}

\begin{priklad}
    Uvažujme množinu klauzúl $S=\{P(x),\ \neg P(x)\}$ a
    interpretácie $I_1 = \{ P(a) \}, I_2 = \{ \neg P(a) \}$.

    Množina $S$ nie je splnená ani jednou interpretáciou.
\end{priklad}

